STM: deq wf

ABS: eqof(d)

STM: eqof wf

STM: deq property

STM: eqof eq btrue

STM: eqof equal btrue

ABS: f**(x)

STM: fix wf

STM: fix property

STM: fix-step

STM: fix-connected

STM: strong-subtype-deq

STM: strong-subtype-deq-subtype

STM: nat-deq-aux

ABS: NatDeq

STM: nat-deq wf

STM: atom-deq-aux

ABS: AtomDeq

STM: atom-deq wf

STM: atom2-deq-aux

ABS: Atom2Deq

STM: atom2-deq wf

STM: bool-deq-aux

ABS: BoolDeq

STM: bool-deq wf

ABS: proddeq(a;b)

STM: proddeq wf

ABS: product-deq(A;B;a;b)

STM: product-deq wf

ABS: sumdeq(a;b)

STM: sumdeq wf

STM: subtype-deq

STM: subtype rel-deq

ABS: union-deq(A;B;a;b)

STM: union-deq wf

ABS: deq-member(eq;x;L)

STM: deq-member wf

STM: assert-deq-member

ABS: DS(A)

STM: discrete struct wf

ABS: dstype(TypeNames; d; a)

STM: dstype wf

STM: decidable dstype equal

ABS: dsdeq(d;a)

STM: dsdeq wf

ABS: dseq(d;a)

STM: dseq wf

ABS: x = y

STM: eq ds wf

STM: ds property

ABS: insert(a;L)

STM: insert wf

STM: insert property

STM: no repeats-insert

STM: member-insert

ABS: l-union(eq;as;bs)

STM: l-union wf

STM: member-union

STM: no repeats union

ABS: l-union-list(eq;ll)

STM: l-union-list wf

STM: member-l-union-list

STM: no repeats-union-list

ABS: remove-repeats(eq;L)

STM: remove-repeats wf

STM: remove-repeats property

STM: member-remove-repeats

ABS: list-diff(eq;as;bs)

STM: list-diff wf

STM: list-diff-property

STM: member-list-diff

ABS: IdDeq

STM: id-deq wf

ABS: a = b

STM: eq id wf

STM: eq id self

STM: assert-eq-id

STM: decidable equal Id

STM: eq id test

ABS: IdLnkDeq

STM: idlnk-deq wf

ABS: a = b

STM: eq lnk wf

STM: assert-eq-lnk

STM: decidable equal IdLnk

ABS: isrcvl(l;k)

STM: isrcvl wf

STM: assert-isrcvl

STM: lconnects-transitive

STM: decidable l member

STM: decidable l disjoint

ABS: l_intersection(eq;L1;L2)

STM: l intersection wf

STM: member-intersection

STM: l disjoint intersection

STM: l disjoint intersection2

STM: disjoint-iff-null-intersection

STM: l disjoint intersection implies

STM: l disjoint intersection implies2

ABS: KindDeq

STM: Kind-deq wf

ABS: a = b

STM: eq knd wf

STM: eq knd self

STM: assert-eq-knd

STM: decidable equal Kind

ABS: locl_rcv{locl_rcv_compseq_tag_def:ObjectId}(tg; l; a)

ABS: rcv_locl{rcv_locl_compseq_tag_def:ObjectId}(a; tg; l)

ABS: locl_locl{locl_locl_compseq_tag_def:ObjectId}(b; a)

ABS: rcv rcv compseq tag def

STM: map-concat-filter-lemma1

STM: map-concat-filter-lemma2

ABS: StandardDS

STM: standard-ds wf

ABS: index(L;x)

STM: l index wf

STM: l index hd

STM: select l index

STM: l before l index

STM: l before l index le

ABS: has-src(i;k)

STM: has-src wf

STM: assert-has-src

ABS: hasloc(k;i)

STM: hasloc wf

STM: assert-hasloc

STM: subtype-set-hasloc

ABS: kind-loc(k;i)

STM: kind-loc wf

ABS: LocKnd

STM: LocKnd wf

ABS: locknd-deq()

STM: locknd-deq wf

ABS: let i,k:LocKnd = ik in P(i;k)

STM: locknd-spread wf

STM: locknd-spread wf2

ABS: locknd(i;k)

STM: locknd wf

STM: locknd functionality isrcv

ABS: MaName

STM: MaName wf

ABS: maname-deq()

STM: maname-deq wf

STM: decidable equal MaName

ABS: name-case(n;i,k.A(i;k);j,x.B(j;x))

STM: name-case wf

STM: decidable l disjoint manames

ABS: if nms1 and nms2 overlap then x else y fi

STM: manames-overlap-case wf

STM: manames-overlap-case-symmetry

STM: manames-overlap-nil

STM: manames-overlap-nil2

STM: no repeats mu index

STM: no repeats l index

STM: no repeats l index-inj